es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, P, Q:({e:E| loc(e) = loc(e1)  Id }Prop).
(e:{e:E| loc(e) = loc(e1)  Id }. P(e)  Q(e))  (e(e1,e2].P(e)  e(e1,e2].Q(e)) 

latex

Definitions	t  T, b, P  Q, False, A, x:A. B(x), x(s), P & Q, P  Q, (e <loc e'), loc(e), Id, E, P  Q, A & B, Prop, e  e' , x:A. B(x), e(e1,e2].P(e), first(e), , x. t(x), ES
Lemmas	event system wf, iff wf, existse-between3 wf, es-E wf, not wf, assert wf, es-first wf, es-locl wf, es-le wf, Id wf, es-loc wf, es-le-loc, es-loc-pred, es-locl-iff